Require Import NaturalDeduction.
Require Import Modal.

(*
Question 1:
A very special island is inhabited only by knights and knaves. Knights always tell
the truth, and knaves always lie. You meet two inhabitants: Zeke and Betty.
Zeke claims that Betty is a knave. 
Betty tells you, “I am a knight or Zeke is a knight.”
Use a truth table to determine who is a knight and who is a knave.

Answer:
Z: Zeke is a knight
B: Betty is a knight

First statement gives:    Z <-> ~B
Second statement gives:   B <-> B \/ Z

Z | B | ~B | B \/ Z | Z <-> ~B | B <-> B \/ Z
---------------------------------------------
0 | 0 |  1 |   0    |    0     |    1
0 | 1 |  0 |   1    |    1     |    1
1 | 0 |  1 |   1    |    1     |    0
1 | 1 |  0 |   1    |    0     |    1

Both statements are only true in Row 2 so that Zeke is a knave and Betty is a knight.
*)

Lemma Question2 {M : MModel} {p q r :MProp} : MValid ([](p /\ <>(q \/ r)) -> []p /\ [](<>q \/ <>r)).
Proof.
start.
Impl_Intro.
And_Intro.
Box_Intro.
Box_Elim in H into Box b0.
And_Elim_1 in H0.
assumption.
Box_Intro.
Box_Elim in H into Box b0.
And_Elim_2 in H0.
Diamond_Elim in H1.
Or_Elim in H1.
Or_Intro_1.
Diamond_Intro into Box b1.
assumption.
Or_Intro_2.
Diamond_Intro into Box b1.
assumption.
Qed.

(* 
Question 3:
Show that the modal logic formula
((<>p) /\ (<>q)) -> <>(p /\ q)
is not valid.
Hint: A frame with three elements is sufficient.

Answer:
Consider the frame F with W={1,2,3} and R={(1,2),(1,3)} and the model M=(F,v) with 
v(p)={2} and v(q)={3}. Then M,1 |= <>p since M,2 |= p and (1,2) in R. Furthermore 
M,1 |= <>q since M,3 |= q and (1,3) in R. But <>(p /\ q) is not true at 1 since 
q is not true at 2 and p is not true at 3.
*)